%Por: Roberto Rama
%Enunciado: Modica a la trivia t de manera tal que el usuario u queda registrado como jugador y devuelve un SMS result con
%el contenido de la primer pregunta de la trivia y el siguiente prejo "Hola!
%Tenes 0 pts. ". Por ejemplo, un primer mensaje podra ser: "Hola! Tenes 0
%pts. Como se llama Maradroga? a.Diego b.Fernando c.Ni el se acuerda." El puntaje inicial de
%cualquier jugador nuevo es 0. Solo podran registrarse usuarios que no sean ya
%jugadores de la trivia en cuestion. El usuario u solo puede registrarse en la
%trivia t si la keyword k que enva corresponde a dicha trivia.
\begin{problema}{registrarJugadorT}{t: Trivia, u: Usuario, k: Keyword}{SMS}
	\requiere[correspondeKeyword]{(\exists c \selec keywords(t)) c==k}
	\requiere[noEsteRegistrado]{ u \not\in participantes(t) }
	\medskip
	\modifica{t}
	\medskip
	\asegura{registrarJugadorAux(t,pre(t),u,result)}
\end{problema}

\begin{aux}{registrarJugadorAux}{t,pret: Trivia, u: Usuario, result:SMS}{Bool}{\\
	( mismos (keywords(pret), keywords(t)) )\\
	\ylogico( mismos (u : participantes(pret), participantes(t)) )\\
	\ylogico( ganadores(pret) == ganadores(t) )\\
	\ylogico( preguntas(pret) == preguntas(t) )\\
	\ylogico( preguntas(t)_0 == proxPregunta(t,u) )\\
	\ylogico( puntajeAcumulado(t,u) == 0 )\\
	\ylogico( losDemasMismosPuntajes(t,pret,u) )\\
	\ylogico (losDemasMismasPreguntas(t,pret,u)) \\
	\ylogico( nroDestino(result) == u )\\
	\ylogico( texto(result) == \!''Hola!\ Tenes\ 0\ pts.\ \!'' ++
	texto(proxPregunta(t,u) )
	}
\end{aux}

%Revisado y aprobado por Mata; 22 de Septiembre. 